D:Dsys, i:Id, k:Knd. Feasible(D)  ((d-decl(D;i)(k)) r M(i).da(k)) 

latex

Definitions	x:A. B(x), P  Q, t  T, Feasible(D), P & Q, A c B,
Lemmas	d-decl-subtype, d-feasible wf, Knd wf, Id wf, dsys wf